Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    a__2nd(cons1(X,cons(Y,Z)))  → mark(Y)
2:    a__2nd(cons(X,X1))  → a__2nd(cons1(mark(X),mark(X1)))
3:    a__from(X)  → cons(mark(X),from(s(X)))
4:    mark(2nd(X))  → a__2nd(mark(X))
5:    mark(from(X))  → a__from(mark(X))
6:    mark(cons(X1,X2))  → cons(mark(X1),X2)
7:    mark(s(X))  → s(mark(X))
8:    mark(cons1(X1,X2))  → cons1(mark(X1),mark(X2))
9:    a__2nd(X)  → 2nd(X)
10:    a__from(X)  → from(X)
There are 13 dependency pairs:
11:    A__2ND(cons1(X,cons(Y,Z)))  → MARK(Y)
12:    A__2ND(cons(X,X1))  → A__2ND(cons1(mark(X),mark(X1)))
13:    A__2ND(cons(X,X1))  → MARK(X)
14:    A__2ND(cons(X,X1))  → MARK(X1)
15:    A__FROM(X)  → MARK(X)
16:    MARK(2nd(X))  → A__2ND(mark(X))
17:    MARK(2nd(X))  → MARK(X)
18:    MARK(from(X))  → A__FROM(mark(X))
19:    MARK(from(X))  → MARK(X)
20:    MARK(cons(X1,X2))  → MARK(X1)
21:    MARK(s(X))  → MARK(X)
22:    MARK(cons1(X1,X2))  → MARK(X1)
23:    MARK(cons1(X1,X2))  → MARK(X2)
Consider the SCC {11-23}. The constraints could not be solved.
Tyrolean Termination Tool  (0.52 seconds)   ---  May 3, 2006